/* 
 * Copyright 2014 Josef Hertl.
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *      http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */
package caetus.modelChecking.goal;

import caetus.modelChecking.variable.ModelVariable;
import java.util.List;

/**
 *
 * @author Josef Hertl
 */
public class ModelGoal {
    /**
     * @return hlpsl-ready presentation of the goals for the model.
     */
    public String makeGoal() {
        String result = "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n\ngoal\n\n";
        result += "secrecy_of ";
        List<ModelVariable> secrets = ModelGoalMap.getProtocolIDs();
        for (int i = 0; i < secrets.size(); i++) {
            if (i!=0) {
                result += ",";
            }
            result += secrets.get(i).getVariableName();
        }
        result += "\n\nend goal\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n";
        return result;
    }
}
